Nuprl Lemma : rel_or_idempotent 11,40

T:Type, R:(TT). R  R  R 
latex


Definitionst  T, Type, x:AB(x), f(a), P  Q, left + right, P  Q, P  Q, , x:A  B(x), P & Q, P  Q, x:AB(x), x f y, R1  R2, R1  R2

origin